<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>MinGeneratedProofStmt</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="MinGeneratedProofStmt";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/gmff/MinFooterStmt.html" title="class in mmj.gmff"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/gmff/MinHeaderStmt.html" title="class in mmj.gmff"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/gmff/MinGeneratedProofStmt.html" target="_top">Frames</a></li>
<li><a href="MinGeneratedProofStmt.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.gmff</div>
<h2 title="Class MinGeneratedProofStmt" class="title">Class MinGeneratedProofStmt</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li><a href="../../mmj/gmff/MinProofWorkStmt.html" title="class in mmj.gmff">mmj.gmff.MinProofWorkStmt</a></li>
<li>
<ul class="inheritance">
<li>mmj.gmff.MinGeneratedProofStmt</li>
</ul>
</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<hr>
<br>
<pre>public class <span class="strong">MinGeneratedProofStmt</span>
extends <a href="../../mmj/gmff/MinProofWorkStmt.html" title="class in mmj.gmff">MinProofWorkStmt</a></pre>
<div class="block">General object representing a Generated Proof statement on a
 <code>MinProofWorksheet</code>.
 <p>
 Generated Proof statements are generated by mmj2 Proof Assistant when the
 user presses Ctrl-U (Unify) and unification successfully creates a Metamath
 proof -- which is simply a RPN (Reverse Polish Notation) list of Metamath
 statement labels. The Generated Proof statement consists of "$=" in column 1
 of the first line of the Generated Proof statement followed by the
 space-separated list of statement labels.
 <p>
 Nothing is typeset by GMFF, and the labels are output as if they were just
 text, or comments (unlike the Metamath Proof Explorere web pages which
 contain hyperlinks for the statement labels.)</div>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colOne" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colOne"><code><strong><a href="../../mmj/gmff/MinGeneratedProofStmt.html#MinGeneratedProofStmt(mmj.gmff.MinProofWorksheet, java.lang.String[][])">MinGeneratedProofStmt</a></strong>(<a href="../../mmj/gmff/MinProofWorksheet.html" title="class in mmj.gmff">MinProofWorksheet</a>&nbsp;w,
                     java.lang.String[][]&nbsp;slc)</code>
<div class="block">Standard MinGeneratedProofStmt constructor.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/gmff/MinGeneratedProofStmt.html#buildModelAExport(mmj.gmff.GMFFExporter, java.lang.StringBuilder)">buildModelAExport</a></strong>(<a href="../../mmj/gmff/GMFFExporter.html" title="class in mmj.gmff">GMFFExporter</a>&nbsp;gmffExporter,
                 java.lang.StringBuilder&nbsp;exportBuffer)</code>
<div class="block">Formats export data for the Generated Proof statement according to the
 <code>Model A</code> specifications and loads the data into a specified
 buffer.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_mmj.gmff.MinProofWorkStmt">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;mmj.gmff.<a href="../../mmj/gmff/MinProofWorkStmt.html" title="class in mmj.gmff">MinProofWorkStmt</a></h3>
<code><a href="../../mmj/gmff/MinProofWorkStmt.html#constructStmt(mmj.gmff.MinProofWorksheet, java.util.List)">constructStmt</a>, <a href="../../mmj/gmff/MinProofWorkStmt.html#getCleanedLineString(int)">getCleanedLineString</a>, <a href="../../mmj/gmff/MinProofWorkStmt.html#getCleanedLineString(int, int, int)">getCleanedLineString</a>, <a href="../../mmj/gmff/MinProofWorkStmt.html#isChunkWhitespace(java.lang.String)">isChunkWhitespace</a>, <a href="../../mmj/gmff/MinProofWorkStmt.html#typesetFormulaSymbols(mmj.gmff.GMFFExporter, java.lang.StringBuilder, java.lang.String[], int)">typesetFormulaSymbols</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="MinGeneratedProofStmt(mmj.gmff.MinProofWorksheet, java.lang.String[][])">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>MinGeneratedProofStmt</h4>
<pre>public&nbsp;MinGeneratedProofStmt(<a href="../../mmj/gmff/MinProofWorksheet.html" title="class in mmj.gmff">MinProofWorksheet</a>&nbsp;w,
                     java.lang.String[][]&nbsp;slc)</pre>
<div class="block">Standard MinGeneratedProofStmt constructor.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>w</code> - <code>MinProofWorksheet</code> of which this statement is a part.</dd><dd><code>slc</code> - Array of Array of String representing the lines and "chunks"
            making up the <code>MinProofWorkStmt</code>.</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="buildModelAExport(mmj.gmff.GMFFExporter, java.lang.StringBuilder)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>buildModelAExport</h4>
<pre>public&nbsp;void&nbsp;buildModelAExport(<a href="../../mmj/gmff/GMFFExporter.html" title="class in mmj.gmff">GMFFExporter</a>&nbsp;gmffExporter,
                     java.lang.StringBuilder&nbsp;exportBuffer)
                       throws <a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></pre>
<div class="block">Formats export data for the Generated Proof statement according to the
 <code>Model A</code> specifications and loads the data into a specified
 buffer.
 <p>
 Model A model files for <code>MinGeneratedProofStmt</code> objects are
 "optional", meaning that if any of the model files are not found, the
 export process is continues normally but Generated Proof statements are
 not output as part of the Proof Worksheet export.
 <p>
 Note the quirky handling of <code>modelAGenProof1X</code>. If this model file
 is empty then no data is output at that location. This quirky feature
 will generally not be used but is provided for maximum flexibility in
 creating export format models.
 <p>
 Additional information may be found \GMFFDoc\GMFFModels.txt.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/gmff/MinProofWorkStmt.html#buildModelAExport(mmj.gmff.GMFFExporter, java.lang.StringBuilder)">buildModelAExport</a></code>&nbsp;in class&nbsp;<code><a href="../../mmj/gmff/MinProofWorkStmt.html" title="class in mmj.gmff">MinProofWorkStmt</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>gmffExporter</code> - The <code>GMFFExporter</code> requesting the export data
            build.</dd><dd><code>exportBuffer</code> - The <code>StringBuilder</code> to which exported data is
            to be output.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/gmff/GMFFException.html" title="class in mmj.gmff">GMFFException</a></code> - if errors are encountered during the export
             process.</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/gmff/MinFooterStmt.html" title="class in mmj.gmff"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/gmff/MinHeaderStmt.html" title="class in mmj.gmff"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/gmff/MinGeneratedProofStmt.html" target="_top">Frames</a></li>
<li><a href="MinGeneratedProofStmt.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li>Field&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
